sends ${\it knd}$(v:$T$) on $l$:
\\[0ex]tagged($g$,State(${\it ds}$),v):${\it dt}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr(inr(inr(inr(inr(inr(inl($\langle$${\it ds}$$,\,$${\it knd}$$,\,$$T$$,\,$$l$$,\,$${\it dt}$$,\,$$g$$\rangle$)))))))